| Definitions | M.ef(k,x,s,v)?w, ma-ef-const(M;k;x;s;v), M.state, EState(T), f(x)?z, z != f(x)   P(a;z), M.init(x)?v, constant_function(f;A;B), ma-init-const(M;x), discrete(i;x), (i = j), Msg(M), i <z j, hd(l), ||as||, suptype(S; T),  , locl(a), timedState(ds), M.ds(x), M.(timed)state, act(k), M.da(a), p   q, w.TA, valtype(i;a), w-machine(w;i), let x,y,z = a in t(x;y;z), d-machine(i;M;dec), d-partial-world(D;f;t';s;d), Top, mval(m), mtag(m),   x,y. t(x;y), M.dout2(l;tg), mlnk(m), False, A  B, Action(dec),  T, P  Q, P Q, P Q, {T}, SQType(T), d-comp-partial-world(D; v; sched; dec; discrete; t), True, let x = a in b(x), d-comp(D; v; sched; dec; d), CV(F), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-action-dec(TA;M;i), d-decl(D;i), i  j , doact(k;v), val(a), tag(k), rcv(l,tg), null, x. t(x), lnk(k), isrcv(k), outl(x), p  q, outr(x),  b, isl(x),  b, shift-state(s), ff, tt, if b then t else f fi , A, x(s),  x L. P(x), next-world-state(D;i;s;k;v), S  T, Y, reduce(f;k;as), filter(P;l), onlnk(l;mss), stutter-state(s), kind(a), w.T, w.M, w-discrete-constraint(w), w-atom-constraint(w), w-machine-constraint(w), msg(a), isrcv(l;a), s(i;t).x, vartype(i;x), a(i;t), isnull(a), m(i;t), t.2, t.1, Msg, d-world(D;v;sched;dec;discrete), FairFifo,  , t T,  x:A. B(x), A c B, P & Q, P Q, x:A. B(x), Valtype(da;k), MsgA, d-feasible-discrete(D;discrete), ma-prob-da(M), finite-type(T), Feasible(M), i = j, i j < k, {i..j }, Feasible(D), x(s1,s2), Dec(P), Knd,  , Unit, Msg(da), M.Msg, d-world-state(D;i), read-state(s), M.din(l,tg), M.dout(l,tg),  , msg(l;t;v), a = b |
| Lemmas | ma-state wf, Kind-deq wf, product-deq wf, fpf-sub weakening, subtype-fpf-cap-void, fpf-ap wf, fpf-trivial-subtype-top, fpf-dom wf, id-deq wf, fpf-cap wf, EState wf, subtype rel transitivity, subtype rel list, filter type, locl one one, pi2 wf, inr equal, decidable equal Id, w-knum wf, doact wf, action wf, int seg wf, ma-init-val wf, d-partial-world wf, ma-ef-val wf, msga wf, shift-state wf, Id sq, equal-next-world, next-world-state wf, bool sq, Knd sq, islocal wf, bfalse wf, btrue wf, w-a wf, w-isnull wf, isrcv wf, w-queue-nil, d-comp wf2, CV wf, pos length, assert-d-eq-Loc, w-queue-partial, assert of null, top wf, null wf3, null-action wf, ma-dout2 wf, ma-da wf, kindcase wf, mtag wf, rcv wf, w-queue-wf2, assert of le int, or functionality wrt iff, assert of bor, bnot of lt int, bnot thru band, squash wf, assert of lt int, le int wf, bor wf, d-comp-partial-world wf, lt int wf, d-eq-Loc wf, IdLnk sq, decidable assert, inr eq inl, d-decl wf, Knd wf, locl wf, tagof wf, lnk wf, hd wf, w-queue wf, d-world wf, w-Msg wf, length wf1, ge wf, pi1 wf, d-world-state wf, false wf, true wf, d-msg-subtype, member wf, int inc rationals, qadd wf, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, eq int wf, assert-eq-id, assert-eq-lnk, and functionality wrt iff, assert of band, iff transitivity, not functionality wrt iff, l member wf, band wf, filter is nil, read-state wf, ma-send-val wf, eq id wf, filter filter, d-decl-subtype2, mlnk wf d, ma-msg wf, subtype rel self, msg wf, mlnk wf, eq lnk wf, filter wf, ma-dout wf, Msg wf, not wf, better-d-comp-step, dsys wf, Id wf, ma-tst wf, ma-prob wf, p-outcome wf, ma-prob-dom wf, ifthenelse wf, ma-st wf, bool wf, d-feasible wf, d-feasible-discrete wf, ma-ds wf, rationals wf, constant function wf, outr wf, bnot wf, ma-has-pre wf, outl wf, le wf, unit wf, nat wf, isl wf, lsrc wf, d-m wf, ma-sends-on wf, assert wf, ldst wf, IdLnk wf |
(?(
dec:(i,a:Id
;M(i).ds(x)))